//! Special symbols defined in [`creusot_contracts`] and annotated with
//! `#[creusot::intrinsics = "..."]`

use crate::{contracts_items::get_intrinsic, ctx::TranslationCtx, metadata::Metadata};

use rustc_hir::{def::DefKind, def_id::DefId};
use rustc_middle::ty::TyCtxt;
use rustc_span::{DUMMY_SP, Symbol};
use std::collections::HashMap;

macro_rules! contracts_items {
    ($($symbol:literal $id:ident)*) => {
        #[derive(PartialEq, Eq, Hash, Debug, Copy, Clone)]
        pub enum Intrinsic {
            $($id),*,
            None
        }

        pub(crate) fn gather_intrinsics<'tcx>(tcx: TyCtxt<'tcx>, ext: &Metadata<'tcx>) ->
            (HashMap<Symbol, DefId>, HashMap<Intrinsic, DefId>, HashMap<DefId, Intrinsic>) {
            let raw : HashMap<Symbol, DefId> = tcx
                .iter_local_def_id()
                .filter_map(|did| {
                    let mut did = did.to_def_id();
                    match tcx.def_kind(did) {
                        DefKind::Ctor(..) => did = tcx.parent(did),
                        // Some definitions are not associated to HirIds and cannot have attributes
                        // For these definitions, `get_intrinsic` crashes. So we filter only the
                        // `DefKind`s that we know will not make it crash. This list is not
                        // exhaustive and may need to be extended if we need other kinds of
                        // intrinsics in the future.
                        DefKind::Struct |
                        DefKind::Union |
                        DefKind::Enum |
                        DefKind::Fn |
                        DefKind::AssocFn |
                        DefKind::Trait => (),
                        _ => return None
                    }

                    Some((get_intrinsic(tcx, did)?, did))
                })
                .collect();
            let mut int2did = HashMap::new();
            let mut did2int = HashMap::new();
            let mut missing_items = Vec::new();
            let mut no_items = true;
            $(
                let sym = Symbol::intern($symbol);
                let here = raw.get(&sym).copied();
                let there = ext.intrinsic(sym);
                if here.is_some() && there.is_some() {
                    panic!("An intrinsic is defined twice");
                }
                let did = here.or(there);
                if let Some(did) = did {
                    if int2did.insert(Intrinsic::$id, did).is_some() { panic!() };
                    if did2int.insert(did, Intrinsic::$id).is_some() {
                        panic!("{did:?} has more than one intrinsic declaration.")
                    };
                    no_items = false
                } else {
                    missing_items.push($symbol)
                }
            )*
            if no_items {
                tcx.dcx().struct_span_fatal(DUMMY_SP,
                    "The `creusot_contracts` crate is not loaded. You will not be able to verify any code using Creusot until you do so."
                ).with_note("Don't forget to actually use creusot_contracts: `use creusot_contracts::prelude::*;`").emit()
            } else if !missing_items.is_empty() {
                let mut message =
                    String::from("The `creusot_contracts` crate is loaded, but the following items are missing: ");
                for (i, item) in missing_items.iter().enumerate() {
                    if i != 0 {
                        message.push_str(", ");
                    }
                    message.push_str(item);
                }
                message.push_str(". Maybe your version of `creusot-contracts` is wrong?");
                tcx.dcx().struct_span_fatal(DUMMY_SP, message).emit()
            }
            (raw, int2did, did2int)
        }
    };
}

impl Intrinsic {
    pub fn get(self, ctx: &TranslationCtx) -> DefId {
        ctx.intrinsic2did[&self]
    }

    pub fn is(self, ctx: &TranslationCtx, did: DefId) -> bool {
        self.get(ctx) == did
    }

    /// Returns `true` for intrisics whose body is generated by Creusot, so that we do not
    /// validate its body
    pub fn synthetic(self) -> bool {
        matches!(
            self,
            Intrinsic::Resolve
                | Intrinsic::Inv
                | Intrinsic::StructuralResolve
                | Intrinsic::SizeOfLogic
                | Intrinsic::SizeOfValLogic
                | Intrinsic::AlignOfLogic
                | Intrinsic::IsAlignedLogic
                | Intrinsic::Postcondition
                | Intrinsic::PostconditionMut
                | Intrinsic::PostconditionOnce
                | Intrinsic::HistInv
                | Intrinsic::Precondition
                | Intrinsic::MetadataMatches
        )
    }
}

contracts_items! {
    "align_of_logic"            AlignOfLogic
    "closure_result"            ClosureResult
    "dead"                      Dead
    "equal"                     Equal
    "exists"                    Exists
    "fn_ghost"                  FnGhost
    "fn_ghost_wrapper"          FnGhostWrapper
    "forall"                    Forall
    "ghost"                     Ghost
    "ghost_deref"               GhostDeref
    "ghost_deref_mut"           GhostDerefMut
    "ghost_into_inner"          GhostIntoInner
    "ghost_new"                 GhostNew
    "hist_inv"                  HistInv
    "implication"               Implication
    "index_logic"               IndexLogic
    "index_logic_stub"          IndexLogicStub
    "int"                       Int
    "inv"                       Inv
    "invariant"                 Invariant
    "is_aligned_logic"          IsAlignedLogic
    "is_aligned_logic_sized"    IsAlignedLogicSized
    "is_aligned_logic_slice"    IsAlignedLogicSlice
    "metadata_matches"          MetadataMatches
    "metadata_matches_slice"    MetadataMatchesSlice
    "metadata_matches_str"      MetadataMatchesStr
    "namespace"                 Namespace
    "neq"                       Neq
    "old"                       Old
    "postcondition"             Postcondition
    "postcondition_mut"         PostconditionMut
    "postcondition_once"        PostconditionOnce
    "precondition"              Precondition
    "ptr_own_as_mut"            PtrOwnAsMut
    "ptr_own_as_ref"            PtrOwnAsRef
    "ptr_own_from_mut"          PtrOwnFromMut
    "ptr_own_from_ref"          PtrOwnFromRef
    "resolve"                   Resolve
    "resolve_method"            ResolveMethod
    "seq_literal"               SeqLiteral
    "size_of_logic"             SizeOfLogic
    "size_of_val_logic"         SizeOfValLogic
    "size_of_val_logic_sized"   SizeOfValLogicSized
    "size_of_val_logic_slice"   SizeOfValLogicSlice
    "size_of_val_logic_str"     SizeOfValLogicStr
    "snapshot"                  Snapshot
    "snapshot_deref"            SnapshotDeref
    "snapshot_deref_mut"        SnapshotDerefMut
    "snapshot_from_fn"          SnapshotFromFn
    "structural_resolve"        StructuralResolve
    "tokens_new"                TokensNew
    "trigger"                   Trigger
    "view"                      View
    "view_stub"                 ViewStub
    "variant_check"             VariantCheck
    "well_founded_relation"     WellFoundedRelation
}
